$\forall$$A$:Type, $f$:$a$:$A$ fp$\rightarrow$ Top, ${\it eq}$:EqDecider($A$), $x$:$A$. $x$ $\in$ dom($f$) $\Leftrightarrow$ ($x$ $\in$ fpf{-}domain($f$))